import os
import simsym
import symtypes
import errno
import model
import signal
import ptypes
import Lock
import Semaphore

class SemaphoreTable(simsym.tstruct(
		stbl = symtypes.tmap(ptypes.SEMAID, Semaphore.Semaphore),
		lck = Lock.Lock,
		size = simsym.SInt
                )):
	def _declare_assumptions(self, assume):
		super(SemaphoreTable, self)._declare_assumptions(assume)
	
	@model.methodwrap(l = Lock.Lock)
	def INIT(self, l):
		self.lck = l
		self.size = 0
		return
	
	@model.methodwrap()
	def NewSemaphore(self):
		self.lck.Lock()
		s = Semaphore.Semaphore.var("s")
		s.INIT
		sid = ptypes.SEMAID.var("sid")
		sid = self.size
		self.size = self.size + 1 # GenSemaID
		self.stbl[sid] = s
		self.lck.Unlock()
		return True

	@model.methodwrap()
	def DelSemaphore(self):
		self.lck.Lock()
		#del self.stbl[sid]  #XXX don't know why commuter forbids del
				     # it doesn't matter if we do not really delete
		self.lck.Unlock()
		return True

	@model.methodwrap(sid = ptypes.SEMAID)
	def GetSemaphore(self, sid):
		self.lck.Lock()
		s = self.stbl[sid]
		self.lck.Unlock()
		return s

model_class = SemaphoreTable

